Presented by Becky Straus.

Abstract: Efforts at the federal level to pass laws like the Stop Online Piracy Act (SOPA) and the Cyber Intelligence Sharing and Protection Act (CISPA) have attracted widespread attention and criticism, and rightly so. But Washington, D.C. is far from the only place that officials are making decisions that impact the privacy and free speech rights. State and local officials are jumping into the fray as well, passing laws or creating policies that have immediate impact without the spotlight that accompanies federal action. The fact is that privacy laws have failed to keep up with emerging technologies. This presentation will survey several areas where state and local officials in Oregon have recently been active, including reviewing policies on automated license plate recognition, surveillance cameras, and use of domestic drones. We will discuss how the ACLU of Oregon has been involved and what is on our agenda for the upcoming 2013 state legislative session.

Presented by John Launchbury.

In secure computation, one or more parties collaborate to compute a result while keeping all the inputs private. That is, no-one can gain knowledge about the inputs from the other parties, except what can be determined from the output of the computation. Methods of secure computation include fully homomorphic encryption (where one party owns the input data and the other party performs the whole computation), and secure multiparty computation (where multiple parties collaborate in the computation itself). The underlying methods are still exceedingly costly in time, space, and communication requirements, but there are also many other practical problems to be solved before secure computation can be usable. For programmers, the algorithm construction is often nonintuitive; for compiler writers, the machine assumptions are very different from usual; and for application designers, the application information flow has to match the security architecture. In this talk we will highlight these challenges, and indicate promising research directions.

Presented by Morgan Miller.

Cryptographic tools have become more powerful in the last three decades. With that power has come complexity. To use or even understand most security tools you need a thorough understanding of mathematics which makes them inaccessible to the general public. The discipline of usability has been growing as well in the past three decades. There have been few but promising overlaps in usability and security which may provide vital tools for managing our digital selves, upholding the principal of privacy, and preserving freedom of speech.

abstract: What if you want to store encrypted files on an untrusted Cloud Server in such a way that Server does not even know if you are editing the same file today as you were yesterday, or anything else about your usage patterns other than total amount of traffic to the Server? Clearly, no matter how strong of an encryption you use, access pattern is revealed: Cloud Server can simply track where on the hard drive you read/write from – clearly encryption does not hide that information. One naive solution to prevent revealing access pattern to the Server is to simply read all your data back from the Server and re-write your entire data back to Server in its entirety for each read/write. This works, but it is clearly impractical. Oblivious Random Access Memory (ORAM) is an algorithm that allows you to completely hide arbitrary access pattern in an efficient manner. In this talk, I will describe Oblivious RAM from the ground up, starting from my own Ph.D. thesis work on this topic (STOC 1990, MIT Ph.D. 1992) which showed the first efficient ORAM. The Journal Version of this work gained over 450 references according to Google Scholar [Ostrovsky-Goldreich JACM 1996] and ORAM became an important area of research in Cryptography in the last 5 years. I will describe surprising connections of ORAM to (1) tamper-proof embedded systems, (2) Software Protection (3) Secure Multi-Party and Secure Two Party Computation as well as (4) ways to securely compile programs with loops, “goto” statements, recursion, etc. into Garbled programs without “unrolling” the execution path, yet not revealing anything about the execution path. I will also compare and contrast ORAM to Single-Server Private Information Retrieval (Single-server PIR), which I co-invented with Kushilevitz in 1997, and explain important differences of these two models. The talk will be self-contained and accessible to the general audience.

Speaker bio: Rafail Ostrovsky is a Professor of Computer Science and Professor of Mathematics at UCLA and co-founder of Stealth Software Technologies, Inc. He has over 200 papers published in refereed journals and conferences and has 11 U.S. Patents issued. In 2013, Dr. Ostrovsky was inducted as an IACR (International Association of Cryptologic Research) Fellow. He currently serves as Vice-Chair of the IEEE Technical Committee on Mathematical Foundations of Computing and has served on 38 international conference Program Committees including serving as a PC chair of FOCS 2011. He is a member of the Editorial Board of JACM, the Editorial Board of Algorithmica; and the Editorial Board of Journal of Cryptology; he serves on the Editorial and Advisory Board of the International Journal of Information and Computer Security and is a member of the steering committee of the international symposium of Security in Communication Networks (SCN). He is a recipient of multiple academic awards and honors and has google h-index factor of 55. At UCLA, Prof. Ostrovsky heads security and cryptography multi-disciplinary Research Center (http://www.cs.ucla.edu/security/) at Henry Samueli School of Engineering and Applied Science.

Correct-By-Construction Control Synthesis in Model-Based Design of Autonomous Systems

speaker: Ufuk Topcu

abstract: How can we affordably build trustworthy autonomous, networked systems? Partly motivated by this question, I describe a shift from the traditional "design+verify" approach to "specify+synthesize" in model-based engineering. I then discuss our recent results on automated synthesis of correct-by-construction, hierarchical control protocols. These results account for hybrid dynamics that are subject to rich temporal logic specifications and heterogenous uncertainties, and that operate in adversarial environments. They combine ideas from control theory with those from computer science, and exploit underlying system-theoretic interpretations to suppress the inherent computational complexity. The expressivity of the resulting design methodology enables us to formally investigate a number of emerging issues in autonomous, networked systems. I conclude my talk with a brief overview of several such issues from my ongoing projects: (i) compositional synthesis for the so-called fractionated systems; (ii) effects of perception imperfections on protocol synthesis; (iii) interfaces between learning modules and reactive controllers with provable guarantees of correctness; and (iv) human-embedded autonomy.

bio: Ufuk Topcu is a Research Assistant Professor in the Department of Electrical and Systems Engineering at the University of Pennsylvania. He received his Ph.D. from the University of California, Berkeley and was a Postdoctoral Scholar at the California Institute of Technology until 2012. His research is on the analysis, design, and verification of autonomous, networked systems.

Formal Verification of Cyber-Physical Systems

speaker: Pavithra Prabhakar

abstract: Cyber-Physical Systems (CPS) refer to systems in which control, computation and communication converge to achieve complex functionalities. The ubiquitous deployment of cyber-physical systems in safety critical applications including aeronautics, automotive, medical devices and industrial process control, has pressurized the need for the development of automated analysis methods to aid the design of high-confidence systems. The talk will focus on an important feature of cyber-physical systems, namely, the mixed discrete-continuous behaviors manifesting as a result of the interaction of a network of embedded processors with the physical world. Hybrid Automata are a popular formalism for modeling systems exhibiting both discrete and continuous behaviors. We discuss formal approaches for the verification of hybrid automata. More precisely, scalable approaches based on approximations, including predicate abstraction, counter-example guided abstraction refinement and bounded error approximations, will be discussed in the context of safety and stability analysis. We will present applications of the techniques on hybrid automata models.

bio: Pavithra Prabhakar is on the faculty at the IMDEA Software Institute in Madrid, Spain, since 2011. Previously, she obtained her doctorate in Computer Science from the University of Illinois at Urbana-Champaign, from where she also obtained a masters in Applied Mathematics. She has a masters degree in Computer Science from the Indian Institute of Science, Bangalore and a bachelors degree from the National Institute of Technology, Warangal, in India. She spent the year between 2011-2012 at the California Institute of Technology as a CMI (Center for Mathematics of Information) fellow. Her main research interest is in Formal Analysis of Cyber-Physical Systems, more precisely, hybrid systems, with focus on both theoretical and practical aspects.

speaker: Joachim Breitner

abstract: We will take you on a guided tour through the memory of a running Haskell program and get to peek at the raw bytes of Haskell values. We’ll see how uniformity allows for polymorphic functions and data structures, where the garbage collector finds the information it needs and learn to predict how large certain values tend to become. With the help of a visualization tool (ghc-vis) we will also see laziness and sharing at work, and reveal the mystery of how Haskell fits infinite data structures into a finite amount of memory.

bio: Joachim Breitner is a PhD student at the Karlsruhe Institute of Technology, Germany, where he works on the semantics of lazy functional programming language and on interactive theorem provers. He maintains the Haskell packages for Debian and Ubuntu and contributes to GHC. When he is AFK, he enjoys board games, swing dancing, softball and paragliding.

abstract: Sunroof is an embedded Haskell Domain Specific Language (DSL) that compiles to JavaScript. Blank Canvas is an embedded Haskell DSL that provides direct access to the HTML5 JavaScript Canvas. Both DSLs superficially provide the same capabilities, but make different trade-offs in the DSL design space. Sunroof uses monadic reification to enable bindings in the DSL to be translated into bindings in JavaScript, while blank canvas has every binding make a round trip from Haskell, to JavaScript, back to Haskell. In this talk, we will present the specifics of both DSLs, using examples, then use both DSLs to outline the difference choices available when designing and implementing embedded DSLs in Haskell.

bio: Andrew (Andy) Gill was born and educated in Scotland, and has spent his professional career in the United States, working both in industry, and academia. Andy received his Ph.D. from the University of Glasgow in 1996, then spent three years in industry as a compiler developer, and a year in academia as a principal project scientist. He co-founded Galois in 2000, a technology transfer company that used language technologies to create trustworthiness in critical systems. In 2008, he joined the University of Kansas, and in 2014 he was a recipient of the NSF CAREER Award.

Andy believes that functional languages like Haskell are a great medium for expressing algorithms and solving problems. Since returning to academia, he has targeted the application areas of telemetry and signal processing, specializing in generating high performance circuits from specifications. His research interests include optimization, language design, debugging, and dependability. The long-term goal of his research is to offer engineers and practitioners the opportunity to write clear and high-level executable specifications that can realistically be compiled into efficient implementations.

Abstract: Records in Haskell are notoriously difficult to compose; many solutions have been proposed. Vinyl lies in the space of library-level approaches, and addresses polymorphism, extensibility, effects and strictness. I describe how Vinyl approaches record families over arbitrary key spaces using a Tarski universe construction, as well as a method for immersing each field of a record in a chosen effect modality. Moreover, I give a characterization of records as sheaves of types, which provides a clear motivation for the safety of subtyping and coercion of records, and a path toward records with non-trivial topologies on their key spaces. Lastly, I describe an interpretation of Vinyl-style records into Type Theory as finite products over containers, leading to many possible and interesting extensions, such as compositional universes of polymorphic variants, as well as inductive and coinductive types.

Bio: I'm an amateur type theorist who studied Historical Linguistics during my undergraduate at UC Berkeley, specializing in Ancient Greek, Sumerian, Akkadian and Anglo-Saxon. I'm particularly interested in type-theoretic syntax and semantics for natural language, and am presently exploring the use of multi-modal combinatory categorial grammar for interpreting the hyperbaton-rich syntax of ancient Indo-European languages. In addition to my interest in linguistics, I have become obsessed with extensionality, realizability and PER semantics for Martin-Löf Type Theory, and am currently trying to come up with an extension to Observational Type Theory which internalizes further extensional concepts, such as union, intersection, image and PER types whilst retaining decidability of type checking.

abstract: C programs are notoriously difficult to reason about, either for safety or full functional correctness. Even with a program logic powerful enough to prove the necessary properties, the proof has the assumption that the compiler behaves exactly the way it is expected to. Verified Software Toolchain (VST) answers this problem by providing a logic specified at the source level that proves properties about generated assembly code. It is proved sound w.r.t. the operational semantics of C, the same operational semantics compiled by the proved-correct CompCert verified optimizing C compiler. Both of those proofs are machine-checked in Coq, an interactive proof assistant. This talk will present the basics of VST, followed by an example proof of a C program.

bio: Josiah (Joey) Dodds is an intern at Galois for the summer, researching the verification of cryptographic libraries. After the summer he will return to finish his PhD at Princeton, where he has been verifying information-flow properties and C programs in Coq.

abstract: Automatic device driver synthesis is a radical approach to creating drivers faster and with fewer defects by generating them automatically based on hardware device specifications. I will present the design and implementation of a new driver synthesis toolkit, called Termite-2. Termite-2 is the first tool to combine the power of automation with the flexibility of conventional development. It is also the first practical synthesis tool based on abstraction refinement. Finally, it is the first synthesis tool to support automated debugging of input specifications. I will explain the main principles behind the tool and give a brief demo of its capabilities.

bio: Leonid Ryzhyk is a postdoctoral fellow at the University of Toronto and a researcher at NICTA. He received his PhD from the University of New South Wales in 2010.

Galois is pleased to host the following tech talk. These talks are open to the interested public–please join us! (There is no need to pre-register for the talk.)

abstract: At this year’s WWDC, Apple announced Swift, a new programming language for iOS and OS X development. In this talk, I’d like to give a brief overview of the language, focussing on its ‘functional features’. I’ll try to demonstrate that there are exciting new possibilities for applying functional programming technology to a new platform — like writing an app that computes Fibonacci numbers without using a for-loop.

bio: Wouter Swierstra is a lecturer at the University of Utrecht. He has recently written a book, Functional Programming in Swift, together with Chris Eidhof and Florian Kugler.

abstract: We present four calculi for gradual typing: $\lambda\B$, based on the blame calculus of Wadler and Findler~(2009); $\lambda\C$, based on the coercion calculus of Henglein~(1994); and $\lambda\T$ and $\lambda\W$, based on the threesome calculi with and without blame of Siek and Wadler~(2010). We define translations from $\lambda\B$ to $\lambda\C$, from $\lambda\C$ to $\lambda\T$, and from $\lambda\T$ to $\lambda\W$. We show each of the translations is fully abstract —far stronger correctness results than have previously appeared.

bio: Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh. He is an ACM Fellow and a Fellow of the Royal Society of Edinburgh, past chair of ACM SIGPLAN, past holder of a Royal Society-Wolfson Research Merit Fellowship, and a winner of the POPL Most Influential Paper Award. Previously, he worked or studied at Stanford, Xerox Parc, CMU, Oxford, Chalmers, Glasgow, Bell Labs, and Avaya Labs, and visited as a guest professor in Copenhagen, Sydney, and Paris. He has an h-index of 60, with more than 18,000 citations to his work according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is a co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004) and Generics and Collections in Java (O’Reilly, 2006). He has delivered invited talks in locations ranging from Aizu to Zurich.

abstract: Read-copy update (RCU) is a synchronization mechanism that is sometimes used as an alternative to reader-writer locking (among other things) that was added to the Linux kernel in 2002. A similar mechanism was added to Sequent’s DYNIX/ptx parallel UNIX kernel in 1993, and antecedents go back to at least 1980. Although a fully functional textbook implementation of RCU comprises only about 20 lines of code, the Linux-kernel implementation comprises more than 15,000 lines of code due to harsh requirements involving performance, scalability, energy efficiency, real-time response, memory footprint, module unloading, hotplugging of CPUs, and software-engineering considerations.

Therefore, a key Linux-kernel RCU challenge is validation and verification. To this end, more than 2500 lines of the current Linux-kernel implementation do torture testing. However, there are now more than one billion devices running Linux, so that an RCU bug that manifested on average once every million years of machine time would manifest about three times every day across the installed base. Furthermore, the combination of Internet of Things and Josh Triplett’s Linux Kernel Tinification project is likely to significantly increase the number of running instances.

I write and run rcutorture tests myself, and I like to think that my 20 years of parallel-code testing experience allows me to meet this validation challenge, but a simple analysis suggests a gap of several orders of magnitude. Additional validation and verification techniques are thus called for. This talk gives a brief overview of RCU and describes my adventures evaluating various verification techniques.

bio: Paul E. McKenney has been coding for almost four decades, more than half of that on parallel hardware, where his work has earned him a reputation among some as a flaming heretic. Over the past decade, Paul has been an IBM Distinguished Engineer at the IBM Linux Technology Center. Paul maintains the RCU implementation within the Linux kernel, where the variety of workloads present highly entertaining performance, scalability, real-time response, and energy-efficiency challenges. Prior to that, he worked on the DYNIX/ptx kernel at Sequent, and prior to that on packet-radio and Internet protocols (but long before it was polite to mention Internet at cocktail parties), system administration, business applications, and real-time systems. He has a BS in Computer Science and another in Mechanical Engineering along with an MS in Computer Science, all from Oregon State University. He also has a Ph.D. in Computer Science and Engineering from OGI/OHSU. He has more than 100 publications and more than 50 patents. His hobbies include what passes for running at his age along with the usual house-wife-and-kids habit.

abstract: GHC is a state-of-the-art optimizing compiler that is constantly being improved. But despite all of the hard work by the developers, you occasionally find yourself in need of a feature that GHC does not (yet) support. Luckily for us, GHC does have multiple extension points built into the standard compilation pipeline, in addition to exposing its functionality as a library.

In this talk I’ll give an overview of GHC’s internal architecture and existing extension points. I’ll also walk through a recent extension I wrote to improve the debugging experience in embedded DSLs.

bio: Eric Seidel is a 3rd year PhD student at UC San Diego, where he works on the LiquidHaskell program-verification tool.

abstract: If you do a web search for “encrypting Strings in Android”, you’ll find a lot of example code, and they all look pretty similar. They definitely input a String and output gibberish that looks like encrypted text, but they are often incorrect. Crypto is tricky: it’s hard to tell that the gibberish that’s being printed is not good crypto, and it’s hard to tell that the code example you picked up from Stack Overflow has serious flaws.

The problem here is that sites like Google and Stack Overflow rank results based on popularity, but the correctness of crypto isn’t something we can vote about. It’s not a popularity contest. To use it correctly, you have to understand the properties of the algorithm and the security goals of your code. Maybe the bad crypto someone pasted up on the Internet was acceptable for their needs, but there’s a good chance it’s completely unacceptable for yours.

In this talk, we’ll discuss the use of a very common crypto algorithm, AES, and show how code examples on the Internet usually make serious mistakes in how they use AES libraries. What are the consequences of these mistakes and what are more reasonable defaults. We’ll also talk a bit about our simple Android library that tries to do AES right.

More information on the Tozny blog: http://tozny.com/blog/encrypting-strings-in-android-lets-make-better-mistakes/

bio: Isaac is a security researcher at Galois where he has lead authentication and collaboration projects for the DoD and IC. Isaac earned his master’s degree in Cybersecurity from the University of Maryland, University College, and his B.S. in Computer Science from Ohio State University. In 2013, Isaac founded Tozny, a Galois spin-off company aimed at solving the password conundrum. Easier and more secure than passwords, Tozny replaces passwords with an easy-to-use cryptographic key on a user’s mobile phone.

bio: Evan Wright is a member of the Technical Staff for the Threat Discovery Group of the CERT Coordination Center (CERT/CC). The CERT/CC is a division of the Software Engineering Institute at Carnegie Mellon University. He holds a MS in Information Security and Technology Management from Carnegie Mellon University and a BS in Technology Systems from East Carolina University. He has over 20 years experience in computer networking and holds a CCNP and six other certifications. Since joining SEI, he has supported a variety of customers in areas such as IPv6 security, ultra-large scale network monitoring, malicious network traffic detection, intelligence fusion, and cybersecurity applications of machine learning. Before joining SEI, he was a network administrator for a medium sized company and Internet Service Provider in North Carolina.

abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as well as using its development tools. Topics to be covered include the basics of dependent types, embedding DSLs in Idris, Idris’s notion of type providers, a general outline of the implementation strategy, the C FFI, and the effects library. Each talk has an associated set of exercises as well as suggested projects for further learning. Participants are expected to be familiar with functional programming in either Haskell or an ML.

bio: David Raymond Christiansen is a Ph.D. student at the IT University of Copenhagen. For the last few months, he has been an intern at Galois, working on verifiable elections and better user interfaces for DSLs. His interests include functional programming languages, domain-specific languages, and environments that make them useful. David has contributed features such as type providers and error reflection to the Idris language as well as significant parts of the Emacs-based IDE. Additionally, he is a co-host of The Type Theory Podcast.

abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as well as using its development tools. Topics to be covered include the basics of dependent types, embedding DSLs in Idris, Idris’s notion of type providers, a general outline of the implementation strategy, the C FFI, and the effects library. Each talk has an associated set of exercises as well as suggested projects for further learning. Participants are expected to be familiar with functional programming in either Haskell or an ML.

bio: David Raymond Christiansen is a Ph.D. student at the IT University of Copenhagen. For the last few months, he has been an intern at Galois, working on verifiable elections and better user interfaces for DSLs. His interests include functional programming languages, domain-specific languages, and environments that make them useful. David has contributed features such as type providers and error reflection to the Idris language as well as significant parts of the Emacs-based IDE. Additionally, he is a co-host of The Type Theory Podcast.

abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as well as using its development tools. Topics to be covered include the basics of dependent types, embedding DSLs in Idris, Idris’s notion of type providers, a general outline of the implementation strategy, the C FFI, and the effects library. Each talk has an associated set of exercises as well as suggested projects for further learning. Participants are expected to be familiar with functional programming in either Haskell or an ML.

bio: David Raymond Christiansen is a Ph.D. student at the IT University of Copenhagen. For the last few months, he has been an intern at Galois, working on verifiable elections and better user interfaces for DSLs. His interests include functional programming languages, domain-specific languages, and environments that make them useful. David has contributed features such as type providers and error reflection to the Idris language as well as significant parts of the Emacs-based IDE. Additionally, he is a co-host of The Type Theory Podcast.

abstract: Jesse has been using Rust to write a PAM module. He will tell us about what he has learned about working with Rust, and about getting Rust’s lifetime-checking to mesh with external C functions.

bio: Jesse Hallett is a research engineer at Galois. He has extensive experience in web and high-level programming; but has only recently ventured into system programming. It has been said that Rust makes system programming accessible to people who wouldn’t touch C++ with a 12-foot pole. Jesse is one of those people. And he is interested in talking about how Rust helps him to access a wider world of programming.

abstract: For the last several years, speed improvements in computing come mainly from increasing parallelism. Imperative programming, however, makes parallelization very difficult due to the many possible dependencies implied by effects. For decades, pure functional programming has held the promise of parallel execution while retaining the very simple semantics that enables practical, rigorous reasoning. This talk describes a prototype compiler from Haskell (not a library) to low-level hardware descriptions for massively parallel execution on reprogrammable logic devices. The compiler works by monomorphizing, miscellaneous other transformations, and conversion to the vocabulary of cartesian closed categories (CCCs), as captured in a small collection of Haskell type classes. One instance of those classes provides an interpretation as parallel circuits. I will show many examples of simple Haskell programs and corresponding compiler-generated circuits.

bio: Conal Elliott has been working (and playing) in functional programming for more than 30 years. He especially enjoys applying semantic elegance and rigor to library design and optimized implementation. He invented the paradigm now known as “functional reactive programming” in the early 1990s, and then pioneered compilation techniques for high-performance, high-level embedded domain-specific languages, with applications including 2D and 3D computer graphics. The latter work included the first compilation of Haskell programs to GPU code, while maintaining precise and simple semantics and powerful composability, as well a high degree of optimization. Conal earned a BA in math with honors from the College of Creative Studies at UC Santa Barbara in 1982 and a PhD in Computer Science from Carnegie Mellon University in 1990. His latest position was at Tabula Inc, where he worked on chip specification and compiling Haskell to hardware for massively parallel execution until their closure in early 2015. Before Tabula, his positions included Architect at Sun Microsystems and Researcher in the Microsoft Research graphics group. He has also coached couples and led conscious relationship workshops together with his partner Holly Croydon, with whom he now lives on 20 acres in the woods in the California Gold Country. For publications, CV, professional blog, etc, see http://conal.net.

abstract: Portland State Aerospace Society (PSAS) is a student aerospace engineering project at Portland State University. We’re building ultra-low-cost, open source rockets that feature some of the most sophisticated amateur rocket avionics systems anywhere. Learn some of the history of the group, why steering a rocket is very, very hard, what we’re doing to solve that problem.

bio: Open-Source Rocket Scientist. Currently the program manager of the Lab for Interconnected Devices at Portland State University — an electronics rapid prototyping playground for engineering students. Nathan has spent the last 7 years helping build a homegrown space program at PSU through volunteering at the Portland State Aerospace Society (PSAS).

abstract: In this talk, I’ll give an introduction to differential privacy with an emphasis on its relationship to machine learning, and its usefulness outside of privacy. Along the way, I’ll give a taste for the mathematical tools that can be used to achieve differential privacy. My thesis is that anyone who cares about data should care about the tools that the differential privacy literature offers.

bio: Katrina Ligett is an assistant professor of computer science and economics at Caltech. Before joining Caltech in 2011, she did postdoctoral work at Cornell, and she received her PhD in computer science from Carnegie Mellon in 2009. Her primary research interests are in mathematical foundations for data privacy, and in game theory. She has received an NSF Career Award, a Microsoft Research Faculty Fellowship, a Google Faculty Research Award, and an Okawa Foundation Research Grant.

abstract:

CH2O is the PhD project of Robbert Krebbers and has as its goal a formal version of the ISO standard of the C programming language. A problem with this is that the C standard is fundamentally inconsistent.

There are three versions of the CH2O semantics: a (small step) operational semantics, an executable semantics, and an axiomatic semantics (a separation logic for C). The most important properties — soundness and completeness results, subject reduction and progress, correctness of the type checker — have all been proved. All definitions and proofs have been fully formalized in Coq, without any axioms and on top of a non-trivial support library.

The CH2O project has two abstract C-like languages. A significant subset of C called “CH2O abstract C” is translated into a simplified language called “CH2O core C”. This translation is written in Coq and implicitly gives a semantics to CH2O abstract C. The rest of the formalization is all about CH2O core C.

The executable CH2O semantics has been extracted to OCaml and combined with the CIL parser to a standalone “interpreter”. This tool can be used to explore all behaviors of a program according to the C standard. Although the CH2O semantics does not yet support I/O (nor the exit function), a small hack allows the CH2O interpreter to still explore programs that call printf.

The CH2O semantics has been specifically designed to be compatible with the CompCert semantics for C. Significant differences between CompCert and CH2O are that the CH2O semantics has explicit typing judgments for everything, and that CH2O applies to any ISO compliant compiler.

bio:

I have a master degree in mathematics (my thesis was about conformal supergravity), and a PhD in computer science, both from the University of Amsterdam. I also worked as a system administrator at the University of Utrecht.

Currently I’m an assistant professor of computer science at the Radboud University Nijmegen. My research has been mainly about formalization of mathematics using interactive theorem provers, but recently I have been getting interested in practical program verification, where interactive proof is used when automation doesn’t cut it.

At the moment I am an alternate member of WG14, and I won a price in the IOCCC twice. And my favorite project is the CakeML/verified-HOL Light project.

abstract:

The last decade has seen many success stories for verified programming with dependent types, including the CompCert verified C compiler, verified libraries for concurrency and security, and machine-checked proofs of results like the four color theorem and the Feit-Thompson theorem. Despite these successes, dependently typed languages are rarely used for day-to-day programming tasks. In this talk, I’ll describe several limitations of modern dependently-typed languages that are holding them back from wider adoption for practical programming. I’ll explain the historical and mathematical reasons for these limitations, and describe how we attempted to relax them in the design of the Zombie research language.

bio:

Chris Casinghino is a Senior Member of the Technical Staff at Draper Laboratory, where he develops static analysis tools in Haskell. In 2014, he completed a PhD in the programming languages group at The University of Pennsylvania. His doctoral research focused on dependently typed programming languages, exploring both their semantics and how to use them to write better programs.

abstract:

Animal movement is driven by responses to both social and non-social factors of the environment. Research across species shows that animals do not make decisions based solely on present information, e.g., at time t, but on an integrated assessment of information over recent time, e.g., t-1, t-2, etc. This raises the conundrum of how to relate distributions of animals (or humans) to conditions of the environment since prior individual experiences, possibly to unobserved conditions, contribute to the behaviors observed. I use a rich animal and environmental data set to harness and integrate the broad spectrum of behavioral research and construct a theoretical platform for describing the observed distributions of species populations. My work in the aquatic, terrestrial, and aerial environments falls into two categories, (i) better managing civil infrastructure that impacts animal movement and (ii) developing/evaluating computational abstractions of environmental sensing and individual decision-making to inform the engineering design of distributed systems in unbounded, open field environments. In the aquatic realm, I’ll share research suggesting that water acceleration “shapes” the individual movement trajectories of juvenile salmon near hydropower dams. Then, I’ll discuss how I am building off this research to understand Sonoran Pronghorn that can interfere with military training activities in the Arizona desert. Lastly, I’ll discuss bird flocking as a biological network that can inform the design of fast, light, mobile, compact, and collapsible systems (e.g., geospatial sensors) that are resilient to attack and can quickly hide.

bio:

R. Andrew Goodwin, PhD LinkedIn: http://www.linkedin.com/in/r-andrew-goodwin-a7524491

abstract:

The Curry-Howard Isomorphism motivates the well known proofs-as-programs interpretation. Under that interpretation, sufficiently different proofs yield different programs. This work is a step toward extracting monadic programs from proofs. In working with the list monad as a motivating example, we discovered that the standard type bind (M a -> (a -> M b) -> M b) does not contain enough information to allow many proofs to go through. For lists, an implicit assumption on the function of type ( a -> M b) is that the input of type a is an element of the list of type M b. We developed an new typeclass of epsilon-monads to be able to strengthen the function type. Epsilon-monads are monads that support a membership predicate. Epsilon-monads enabled the development of a bind-induction proof rule which allows the extraction of monadic programs using the bind operator. Also, epsilon monads allow for extensional specifications of monadic programs. We used the Coq theorem prover to formalize the definitions and to prove many properties of the formalization. This is joint work with Hadi Shafe’i.

bio:

James Caldwell is Professor and Head of the Computer Science Department at the University of Wyoming. He earned his PhD from Cornell in the Nuprl group advised by Robert Constable. Before moving to the University of Wyoming in 1998, he was a researcher in the formal methods group at the NASA Langley Research center. He moved to NASA from the Electric Corporate R&D center in Schenectady, NY where he was first exposed to formal verification. He has MS and BS degrees in computer science from SUNY Albany. Before coming to computer science he studied painting and sculpture at the School of the Museum of Fine Arts, Boston.

abstract:

Due to the exponential growth of our ability to collect, centralize, and share data in recent years we have been able tackle problems previously assumed to be insurmountable. Ubiquitous sensors, fast and efficient machine learning, and affordable commercial-off-the-shelf technologies have not only deepened our understanding of our world, but also democratized these capabilities. As a direct result of this shift, we are facing a rapidly evolving host of challenges centered around our new data-driven world. In this talk we will discuss efforts from the Trustworthy Data Engineering Laboratory (TRUST Lab) in conjunction with our partners at the World Bank, the Federal Bureau of Investigation (FBI), the Environmental Protection Agency (EPA), and the City of Cincinnati to identify and solve problems in Adversarial Machine Learning and Data Science. We will examine real case studies in debarrment and corruption in international procurement with the World Bank, cases of violations of the Resource Conservation and Recovery Act with the EPA, and human rights abuses of low income citizens by corporate slum-lords in the city of Cincinnati. In each of these cases we will show how malicious actors manipulated the data collection and data analytics process either through misinformation, abuse of regional corporate legal structures, collusion with state actors, or knowledge of underlying predictive analytics algorithms to damage the integrity of data used by machine learning and predictive analytic processes, or the outcomes derived from these processes, to avoid regulatory oversite, sanctions, and investigations launched by national and multi-national authorities. This new type of attack is growing increasingly common, and we will motivate and encourage increased research on counter measures and safe guards in information systems.

Additionally we will discuss our efforts to combat problems in data privacy and availability in modern systems, highlighting the tradeoffs involved between data availability and privacy, and introduce a new formal logic for privacy preserving data operations, and demonstrate their performability and correctness, along with metrics for their improved privacy and suitability for high-assurance areas of data science.

bio:

Dr. Eric Rozier is an Assistant Professor of Electrical Engineering and Computing Systems and head of the Trustworthy Data Engineering Laboratory at the University of Cincinnati in Cincinnati, Ohio. He has previously been named a Frontier’s of Engineering Education Faculty member by the National Academy of Engineering, a two time Eric and Wendy Schmidt Data Science for Social Good Faculty Fellow at the University of Chicago, and an IBM Research Fellow. Dr. Rozier’s research interests revolve around the intersection of Data Science and Engineering with Cybersecurity, Reliability, and Performability Engineering, with a focus on dependable computing for critial infrastructures. His work in Adversarial Machine Learning was recently featured as one of the inaugural talks for the USENIX Engima conference on emerging threats and novel attacks. Before joining the University of Cincinnati, Dr. Rozier was the founding director of the Fortinet Cybersecurity Laboratory at the University of Miami where he worked to develop and commercialize new technologies in homomorphic encryption for cloud-based systems. He earned his Ph.D. from the University of Illinois at Urbana-Champaign where he worked on applications in fault-tolerance and security with the National Center for Supercomputing Applications, and the Information Trust Institute.

abstract:

Existing modeled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where it runs the flight control software of a high-assurance quadcopter. To provide low latency, the eChronos OS runs with interrupts enabled and provides a preemptive scheduler. In terms of verification, this means that concurrency reasoning is required, which significantly increases the complexity: application and OS instructions may be interleaved with interrupt handler instructions.

In our work we explicitly model the effect of interrupts and their handling by the hardware and OS. We provide a general formal model of the interleaving between OS code, application code and interrupt handlers. We then instantiate this model to formalise the scheduling behavior of the eChronos OS, and prove the main scheduler property: the running task is always the highest-priority runnable task.

bio:

June Andronick is a Senior Researcher at Data61|CSIRO (formerly NICTA). Her research focuses on increasing the reliability of critical software systems, by mathematically proving that the code behaves as expected and satisfies security and safety requirements. She contributed to the seL4 correctness proof and now focuses on concurrency reasoning for OS code. She leads the concurrency software verification research in Data61, and is deputy leader of the Trustworthy Systems group. She was recognised in 2011 by MIT’s Technology Review as one of the world’s top young innovators (TR35). She holds a PhD in Computer Science from the University of Paris-Sud, France.

abstract:

Hoare monitors, invented by Hansen and Hoare in 1973, are widely used to safely handle concurrent programming in different languages ranging from C++11 to Tower, an EDSL developed by Galois as part of the High-Assurance Cyber Military Systems (HACMS) DARPA program. This talk will explain how basic safety properties are assured using Tower, and how it is possible to improve runtime efficiency and parallelism of Tower-generated C programs by releasing some constraints on the Hoare monitor model. Finally, some test results on SMACCMPilot, a high-assurance autopilot, will be presented.

bio:

Georges-Axel Jaloyan is a CS student at École Normale Supérieure in Paris. He is interning at Galois as part of his Master’s degree. He is interested in embedded systems security and safety-critical systems. He interned previously at NASA Langley Safety Critical Avionics Systems Branch.

abstract:

The domain of Internet of Things (IoT) is rapidly expanding beyond research and becoming a major industrial market with such stakeholders as major manufacturers of chips and connected objects, and fast-growing operators of low-power wide-area networks. Importantly, this emerging domain is driven by applications that leverage the infrastructure to provide users with innovative, high-value services. Because of this application-centric approach, software development plays a key role to realize the full potential of IoT.

In this talk, we argue that there is a continuum between orchestrating connected objects in the small and in the large, fostering a unified approach to application development. We examine the requirements for orchestrating connected objects and address them with domain-specific design concepts. We then show how to map these design concepts into dedicated programming patterns and runtime mechanisms.

Our work revolves around domain-specific notations integrated into a tool-based design methodology, dedicated to develop IoT applications. We have applied our work across a spectrum of infrastructure sizes; we present examples, ranging from an automated pilot in avionics, to an assisted living platform for the home of seniors, to a parking management system in a smart city.

bio:

Charles Consel is a professor of Computer Science at Bordeaux Institute of Technology. He served on the faculty of Yale University, Oregon Graduate Institute and the University of Rennes.

His research contributions cover programming languages, software engineering, operating systems, pervasive computing, and assistive computing.

He leads the Phoenix group at Inria that conducts multi-disciplinary research to design, develop, deploy and assess assistive computing support. This research combines (1) Cognitive Science to study user needs and make a rigorous assessment of assistive services; (2) Sensing and actuating expertise to support the user, based on accurate and rich interactions with the environment; (3) Computer Science to support and guide the development process of the assistive services.

abstract:

Security-critical applications constantly face threats from exploits in lower computing layers such as the OS and Hypervisor, or even attacks from malicious administrators. To protect sensitive data from such privileged adversaries, there is increasing development of secure hardware primitives, such as Intel SGX. Intel SGX instructions enable user mode applications to package trusted code and data into regions that are isolated from all other software on the machine, and also provide cryptographic primitives such as remote attestation. Our research is developing a principled approach to building cloud services with end-to-end security guarantees, including only these trusted hardware primitives in our trusted computing base. In this talk, I will demonstrate how one can use compiler and verification techniques to develop formally verified SGX programs, and demonstrate applications where Map-Reduce programs running on SGX can be certified to not leak secrets.

bio:

Rohit Sinha is currently pursuing a Ph.D. in EECS at UC Berkeley, where he works with Prof. Sanjit Seshia. His research interests include programming languages, software verification, and security.

abstract:

Project E3DB is a tool for programmers who want to build an end-to-end encrypted database with sharing into their projects. We are providing a command-line client for you to play with and a Java SDK to prototype with. Over the next few weeks, we’ll be getting feedback from you, adding features, and making it ready for production.

In this talk, Isaac will discuss what E3DB is, where it’s going, and provide a tutorial for trying it out. Bring your laptop to try!

More on E3DB: https://tozny.com/blog/announcing-project-e3db-the-end-to-end-encrypted-database/

Tozny is a Galois product spin-off. Our mission is to make strong crypto easy for both developers and end users.

bio:

Isaac is a security researcher at Galois where he has lead authentication and collaboration projects for the DoD and IC. Isaac earned his master’s degree in Cybersecurity from the University of Maryland, University College, and his B.S. in Computer Science from Ohio State University. In 2013, Isaac founded Tozny, a Galois spin-off company aimed at solving the password conundrum. Easier and more secure than passwords, Tozny replaces passwords with an easy-to-use cryptographic key on a user’s mobile phone.

Title:

Formally Verifying Implementations of Distributed Systems

Abstract:

Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. In this talk, we'll survey the Verdi project which provides a framework for implementing and formally verifying implementations of distributed systems in Coq. Verdi eases the verification burden by enabling developers to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. Using this approach, the Verdi team produced the first correctness proof for an implementation of the Raft distributed consensus protocol.

Bio:

Zach Tatlock is an Assistant Professor in Computer Science and Engineering at the University of Washington where he leads the Programming Languages and Software Engineering (PLSE) group. He received his PhD from UC San Diego and BS from Purdue (where he took nearly every course with Bill Harris!). His research draws upon proof assistants, SMT solvers, and type systems to improve software reliability and security in domains ranging from distributed systems and compilers to web browsers. He can juggle and solve Rubik’s cubes, but not at the same time.